ds:x:Id fp Type, da:k:Knd fp Type, A:ecl-trans-tuple{i:l}(ds;da), n:.
False
 (((ecl-trans-h(A)(n,ecl-trans-init(A)))))
 (L:(event-info(ds;da) List).
 ((ecl-trans-halt2(ds;da;A)(n,L)))
  (L1:(event-info(ds;da) List).
  L1  L  ((ecl-trans-h(A)(n,ecl-trans-state(A;L1))))  False)) 

latex

Definitions	Id, t  T, x. t(x), x:A. B(x), a:A fp B(a), Knd, ecl-trans-tuple{i:l}(ds;da), , False, b, P  Q, event-info(ds;da), l1  l2, ecl-trans-halt2(ds;da;A), A
Lemmas	false wf, nat wf, ecl-trans-tuple wf, Knd wf, fpf wf, Id wf